A:MsgA, x:Id, k:Knd.
(A.frame(k affects x))  Feasible(A)  ((<k, x>  dom((A.2.2.2.2).1))) 

latex

Definitions

False, P  Q, A, x:A. B(x), P & Q, b, t  T, IdLnk, x:AB(x), Id, Knd, x:A  B(x), Void, Type, x.A(x), x. t(x), t.2, IdDeq, f(x)?z, Top, t.1, KindDeq, State(ds), a:A fp B(a), product-deq(A;B;a;b), x  dom(f), xdom(f). v=f(x)   P(x;v), M.da(a), M.state, M.rframe(A.sends tfL of k on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-frame-compat(A;B), Feasible(M), Valtype(da;k), MsgA, <a, b>

Lemmas

ma-feasible wf, not wf, ma-frame wf, msga wf, assert wf, fpf-dom wf, product-deq wf, fpf-trivial-subtype-top, ma-state wf, Kind-deq wf, pi1 wf, top wf, fpf-cap wf, id-deq wf, pi2 wf, Knd wf, Id wf